#define en_Arrive- (GateOpen && !EntranceFree)
#define en_Arrive+ (EntranceFree && !WaitingTicket)
#define en_Enter (WaitingTicket && (FreePlaces > 0) && !GateOpen && !CarInZone)
#define en_Exit (CarInZone && WaitingToPay && !GateOutOpen)
#define en_Leave- (ExitFree && !WaitingToPay)
#define en_Leave+ (GateOutOpen && !ExitFree)

#define fire_Arrive- GateOpen = 0; EntranceFree = 1
#define fire_Arrive+ EntranceFree = 0; WaitingTicket = 1
#define fire_Enter WaitingTicket = 0; FreePlaces = FreePlaces - 1; GateOpen = 1; CarInZone = 1
#define fire_Exit CarInZone = 0; WaitingToPay = 0; FreePlaces = FreePlaces + 1; GateOutOpen = 1
#define fire_Leave- ExitFree = 0; WaitingToPay = 1
#define fire_Leave+ GateOutOpen = 0; ExitFree = 1

bool EntranceFree, GateOpen, WaitingTicket, CarInZone, WaitingToPay, GateOutOpen, ExitFree;
int FreePlaces;

init
{
	atomic{
		//como gerar o M0?
	}
	do
	  :: en_Arrive--> atomic{ fire_Arrive- }
	  :: en_Arrive+-> atomic{ fire_Arrive+ }
	  :: en_Enter-> atomic{ fire_Enter }
	  :: en_Exit-> atomic{ fire_Exit }
	  :: en_Leave--> atomic{ fire_Leave- }
	  :: en_Leave+-> atomic{ fire_Leave+ }
	od
}